Boolean Satisfiability (SAT) is probably the most studied of combinatorial optimization/search problems. A combinatorial search problem involves finding a condition with specified properties from a large space of all possible conditions arising from the various combinations of the variables in the system. Accordingly, SAT seeks to find a satisfying logical assignment for a propositional logic formula.
Significant effort has been devoted to providing practical solutions to SAT problems for applications in Electronic Design Automation (EDA) and Artificial Intelligence (AI), particularly to prove the correctness of a given digital logic circuit. As a result, the subject of practical SAT solvers has received considerable research attention, and numerous solver algorithms have been proposed and implemented.
Among existing SAT solvers are GRASP, POSIT, SATO, rel_sat and WalkSAT. GRASP and SATO find significant use in both research and industry. To learn about GRASP and SATO, see the following, each of which is incorporated by reference for its useful background information:                Marques-Silva, J. P., and Sakallah, K. A., “GRASP: A Search Algorithm for Propositional Satisfiability,” IEEE Transactions on Computers, vol. 48, 506-521, 1999.        Zhang, H., “SATO: An Efficient Propositional Prover,” Proceedings of the International Conference on Automated Deduction, pages 272-275, July 1997.Most SAT solvers employ some combination of two main strategies: the Davis-Putnam (DP) backtrack search and heuristic local search. Heuristic local search techniques are not guaranteed to be complete (i.e. they are not guaranteed to find a satisfying assignment if one exists or to prove unsatisfiability if a satisfying assignment does not exist). As a result, complete SAT solvers are based almost exclusively on the DP search algorithm.        
Methods employed by SAT solvers using the DP search algorithm can generally be summarized in three steps: making decisions, searching for implications and resolving conflicts. Making decisions involves assigning variables to either zero or one. Searching for implications involves analyzing variable assignments (i.e., decisions made) to find further assignments that, if made, move the SAT problem closer to solution. Typically, searching for implications is performed by a technique known as Boolean Constraint Propagation (BCP). Resolving conflicts undoes variable assignments that have generated implications setting the same variable to both zero and one in different portions of the logic formula (i.e., a conflict is reached when a decision (variable assignment) generates implications setting the same variable to both zero and one in different portions of the logic formula).
In practice, difficult SAT problems can require SAT solvers to run many weeks or more to find a satisfying solution. This type of run time requirement is simply not practical when numerous problems must be solved, or when problem solutions must be expedited. For this reason, there is a need for a faster SAT solver.
In addition, for most SAT problems, a major portion (greater than 90% in some cases) of SAT solver run time is spent in the BCP process. For this reason, there is a need for a more efficient BCP engine, the BCP engine being key to any successful SAT solver and significantly responsible for overall solver run time.
Further, existing strategies for making decisions are mostly directed to minimizing the number of decisions made. However, minimizing the number of decisions made does not necessarily mean minimizing overall solver run time for a given SAT problem, as one particular sequence of decisions, even if minimal in number, could lead to more BCP operations, therefore resulting in greater overall solver run time. Also, when considering different decision-making strategies, computational overhead must be considered. The time required to develop a certain sequence of assignments could negate the benefit gained from implementing the sequencing strategy. Therefore, there is also a need for a low overhead decision making strategy, one highly optimized for speed and specifically designed to operate with an efficient BCP scheme.